Inference at * 1 
Iof proof for Lemma Agatha Murder Puzzle (JProver)Lori2:


1. Agatha hates Charles
2. Agatha hates Agatha
3. p:Person. p is richer than Agatha  The Butler hates p
4. p:Person. Agatha hates p  Charles hates p
5. p:Person. Agatha hates p  The Butler hates p
6. p:Person. p hates Agatha  p hates The Butler  p hates Charles
7. p, q:Person. p kills q  p is richer than q
8. p, q:Person. p kills q  p hates q
  The Butler kills Agatha & Charles kills Agatha 

latex

 by Jprover 

latex

 .

Definitions

P & Q, x:AB(x), x is richer than y, x:A. B(x), P  Q, left+right, x kills y, A, False, P  Q, x:AB(x)